$\forall$$x$, $y$:Atom1. ($\neg$($\uparrow$$x$ =a1 $y$)) $\Leftarrow\!\Rightarrow$ $x$ $\neq$ $y$ $\in$ Atom1